#include "formule.hpp"

// BEGIN Création de formules simples //////////////////////////////////////////
formule variable(string nom) {
	formule res = new formule_s;
	res->op = o_variable;
	res->nom = new string(nom);
	return res;
}

formule variable(char* nom) {
	formule res = new formule_s;
	res->op = o_variable;
	res->nom = new string(nom);
	return res;
}

formule non(formule arg) {
	formule res = new formule_s;
	res->op = o_non;
	res->arg = arg;
	return res;
}

formule et(formule arg1, formule arg2) {
	formule res = new formule_s;
	res->op = o_et;
	res->arg1 = arg1;
	res->arg2 = arg2;
	return res;
}

formule ou(formule arg1, formule arg2) {
	formule res = new formule_s;
	res->op = o_ou;
	res->arg1 = arg1;
	res->arg2 = arg2;
	return res;
}

formule impl(formule arg1, formule arg2) {
	formule res = new formule_s;
	res->op = o_implique;
	res->arg1 = arg1;
	res->arg2 = arg2;
	return res;
}

formule equiv(formule arg1, formule arg2) {
	formule res = new formule_s;
	res->op = o_equivaut;
	res->arg1 = arg1;
	res->arg2 = arg2;
	return res;
}
// END Création de formules simples ////////////////////////////////////////////


// BEGIN Affichage d'une formule ///////////////////////////////////////////////
// Affichage des opérateurs
string operateur2string(operateur op) {
	switch (op) {
	case o_variable:
		return "var";
	case o_non:
		return "~";
	case o_et:
		return "/\\";
	case o_ou:
		return "\\/";
	case o_implique:
		return "=>";
	case o_equivaut:
		return "<=>";
	}
	return string();
}

// Affichage d'une formule par induction sur son arbre de syntaxe
string formule2string(formule f) {
	switch (f->op) {
	case o_variable:
		return *(f->nom);
	case o_non:
		return "~" + formule2string(f->arg);
	case o_et:
	case o_ou:
	case o_equivaut:
	case o_implique:
		return "("+formule2string(f->arg1)
				+" "+operateur2string(f->op)+" "
				+formule2string(f->arg2)+")";
	}
	return string();
}

// Définition de l'opérateur << pour le type formule
ostream& operator<<(ostream& out, formule f){
	out << formule2string(f);
	return out;
}
// END Affichage d'une formule /////////////////////////////////////////////////


// BEGIN Gestion de la mémoire dynamique des formules //////////////////////////
formule copier(formule f) {
	switch (f->op) {
	case o_variable:
		return variable(* f->nom);
	case o_non:
		return non(copier(f->arg));
	case o_et:
		return et(copier(f->arg1),copier(f->arg2));
	case o_ou:
		return ou(copier(f->arg1),copier(f->arg2));
	case o_implique:
		return impl(copier(f->arg1),copier(f->arg2));
	case o_equivaut:
		return equiv(copier(f->arg1),copier(f->arg2));
	}
	return nullptr;
}

void free_all(formule f) {
	switch (f->op) {
	case o_implique:
	case o_equivaut:
	case o_ou:
	case o_et:
		free_all(f->arg1);
		free_all(f->arg2);
		break;
	case o_non:
		free_all(f->arg);
		break;
	case o_variable:
		delete f->nom;
		break;
	}
	delete f;
}

// END Gestion de la mémoire dynamique des formules ////////////////////////////


////////////////////////////////////////////////////////////////////////////////
//            A PARTIR D'ICI LES FONCTIONS SONT A IMPLEMENTER                 //
////////////////////////////////////////////////////////////////////////////////
ostream& operator<<(ostream& out, const cls_t& cl){
	for(cls_t::const_iterator it=cl.cbegin(); it != cl.cend(); it++)
	{
		out << *it;
	}

	return out;
}

ostream& operator<<(ostream& out, const cnf_t& c){
	for(unsigned int i = 0; i < c.size(); i++)
	{
		out << c[i];
	}

	return out;
}

bool est_dans(const cls_t& c, const cnf_t& f){
	for(unsigned int i = 0; i < f.size(); i++)
	{
		if(f[i] == c)
		{
			return true;
		}
	}

	return false;
}

void numerote(formule f, map<std::string,var_t> & corresp){
	if(f->op == o_variable)
	{
		if (corresp.count(*f->nom) == 0) //Si elle n'est pas dans la map
				{
			corresp[*f->nom] = corresp.size();
				}
	}
	else
	{
		if(f->op != o_non)
		{
			numerote(f->arg1, corresp);
			numerote(f->arg2, corresp);
		}
		else
		{
			numerote(f->arg, corresp);
		}
	}

	/*
   si la formule est une variable
        si [...] lui attribuer un numéro (on peut prendre la taille actuelle de corresp comme numéro) et ajouter la correspondance entre le nom de la variable et ce numéro dans corresp;
        sinon la variable a déjà un numéro, ne rien faire;
    sinon, appeler récursivement la fonction de numérotation sur le ou les argument(s).
	 */

}

lit_t var2lit(var_t v, bool p){
	if(p == true)
	{
		return (v*2);
	}
	else
	{
		return ((v*2) + 1);
	}
}

lit_t neg(lit_t l){
	if(l % 2 == 0)
	{
		return l + 1;
	}
	else
	{
		return l - 1;
	}
}

var_t lit2var(lit_t l){
	if(l%2 == 0)
	{
		return (l/2);
	}
	else
	{
		return ((l-1)/2);
	}
}

bool positif(lit_t l){
	return (l%2==0 ? true : false);
}

bool operator==(cnf_t cnf1, cnf_t cnf2)
{
	if(cnf1.size() != cnf2.size())
	{
		return false;
	}
	for(cnf_t::iterator it1 = cnf1.begin(); it1 < cnf1.end(); it1++)
	{
		if(!est_dans(*it1, cnf2))
		{
			return false;
		}
	}

	return true;
}
